Conversation
| EqTest.for_instr env ~alpha i1 i2 | ||
| if EqTest.for_instr env ~alpha i1 i2 | ||
| then true | ||
| else (warn_uptobad env "instructions do not match"; false) |
There was a problem hiding this comment.
I think we should print the two instructions here, this can be done using EcPrinting.pp_instr.
| EqTest.for_expr env a1 a2 && | ||
| (if EqTest.for_expr env a1 a2 | ||
| then true | ||
| else (warn_uptobad env "if statement conditions do not match"; false) |
There was a problem hiding this comment.
Same remark, with EcPrinting.pp_expr
| in | ||
| if not (f_upto_init env bad pr1.pr_fun pr2.pr_fun) then | ||
| tc_error !!tc ~who:"byupto" "the two function are not equal upto bad"; | ||
| tc_error !!tc ~who:"byupto" "up to bad tactic failed"; |
There was a problem hiding this comment.
I have tried this, patch and I see not error message, excepted up to bad tactic failed.
Did you see something else?
I not use to the function EcEnv.notify. Can someone provide hint ?
There was a problem hiding this comment.
I think that proof general does not display the warnings when there is an error. Anyway, the notify mechanism should not be used for extending the error message. Assume that you do a try upto, then you will end with a lot of warning messages that you don't want to see.
There was a problem hiding this comment.
Maybe we should brainstorm a bit about how to manage the communication with the user when launching tactics that do complex analysis. This includes upto, but also circuit-based analysis, sim, etc.
Clearly we need a bit more than yes/no as an answer because these tactics typically require some trial and error before the analysis goes through.
This could be a different mechanism than applying the tactic? Something in the same plane as search for example?
4 participants
This is a rough attempt at improving the warnings of the up to bad tactic.
Need advice what what the correct warning mechanism should be.
The current form helped me sort out a difficulty I had with a proof, but probably needs work.